%------------------------------------------------------------------------------
% File     : LCL634^1 : TPTP v3.7.0. Released v3.6.0.
% Domain   : Logical Calculi
% Problem  : Goedel's ontological argument on the existence of God
% Version  : [Ben08] axioms : Especial.
% English  :

% Refs     : [Fit00] Fitting (2000), Higher-Order Modal Logic - A Sketch
%          : [Ben08] Benzmueller (2008), Email to G. Sutcliffe
% Source   : [Ben08]
% Names    : Fitting-HOLML-Ex-God-alternative-b [Ben08]

% Status   : Theorem
% Rating   : 1.00 v3.7.0
% Syntax   : Number of formulae    :   48 (   3 unit;  27 type;  19 defn)
%            Number of atoms       :  323 (  19 equality;  60 variable)
%            Maximal formula depth :   13 (   5 average)
%            Number of connectives :   71 (   3   ~;   1   |;   2   &;  64   @)
%                                         (   0 <=>;   1  =>;   0  <=;   0 <~>)
%                                         (   0  ~|;   0  ~&;   0  !!;   0  ??)
%            Number of type conns  :  118 ( 118   >;   0   *;   0   +)
%            Number of symbols     :   28 (  27   :;   0  :=)
%            Number of variables   :   51 (   2 sgn;   6   !;   4   ?;  41   ^)
%                                         (  51   :;   0  :=;   0  !>;   0  ?*)

% Comments :

%------------------------------------------------------------------------------
%----Include simple maths definitions and axioms
include('Axioms/LCL008^0.ax').
%------------------------------------------------------------------------------
%----$tType
thf(a,type,
    a: $tType )).

%----The type role and global typing of constants
thf(p,type,(
    p: ( a > $i > $o ) > $i > $o )).

thf(g,type,(
    g: a > $i > $o )).

thf(e,type,(
    e: ( a > $i > $o ) > a > $i > $o )).

%----$i and $o
thf(r,type,(
    r: $i > $i > $o )).

%----> for function types
thf(mall_aio,type,(
    mall_aio: ( ( a > $i > $o ) > $i > $o ) > $i > $o )).

thf(mall_a,type,(
    mall_a: ( a > $i > $o ) > $i > $o )).

%----Local typing of variables and ^ as the lambda binder
thf(mall_aio,definition,
    ( mall_aio
    = ( ^ [P: ( a > $i > $o ) > $i > $o,W: $i] :
        ! [X: a > $i > $o] :
          ( P @ X @ W ) ) )).

thf(mall_a,definition,
    ( mall_a
    = ( ^ [P: a > $i > $o,W: $i] :
        ! [X: a] :
          ( P @ X @ W ) ) )).

%----@ for application
thf(positiveness,axiom,
    ( mvalid
    @ ( mall_aio
      @ ^ [X: a > $i > $o] :
          ( mimpl @ ( mnot @ ( p @ X ) )
          @ ( p
            @ ^ [Z: a] :
                ( mnot @ ( X @ Z ) ) ) ) ) )).

thf(g,definition,
    ( g
    = ( ^ [Z: a] :
          ( mall_aio
          @ ^ [X: a > $i > $o] :
              ( mimpl @ ( p @ X ) @ ( X @ Z ) ) ) ) )).

thf(e,definition,
    ( e
    = ( ^ [X: a > $i > $o,Z: a] :
          ( mall_aio
          @ ^ [Y: a > $i > $o] :
              ( mimpl @ ( Y @ Z )
              @ ( mbox @ r
                @ ( mall_a
                  @ ^ [W: a] :
                      ( mimpl @ ( X @ W ) @ ( Y @ W ) ) ) ) ) ) ) )).

thf(thm,conjecture,
    ( mvalid
    @ ( mall_a
      @ ^ [Z: a] :
          ( mimpl @ ( g @ Z ) @ ( e @ g @ Z ) ) ) )).

%------------------------------------------------------------------------------